Equational Logic
----------------

<!--
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.

SPDX-License-Identifier: CC0-1.0
-->

[(Up)](../../README.md#topics) | _See also: [Logic](../Logic/README.md#logic), [Term Rewriting](../Term%20Rewriting/README.md#term-rewriting), [Universal Algebra](../Universal%20Algebra/README.md#universal-algebra)_

- - - -


### Web resources

[Equational Logic \-- from Wolfram MathWorld](https://mathworld.wolfram.com/EquationalLogic.html) ★

[Equational logic - Wikipedia](https://en.wikipedia.org/wiki/Equational_logic)

[Algebraic theory - Wikipedia](https://en.wikipedia.org/wiki/Algebraic_theory)

[predicate logic - Give an equational proof \$ \\vdash (\\forall x)(A \\rightarrow B) \\equiv ((\\exists x) A) \\rightarrow B\$ - Mathematics Stack Exchange](https://math.stackexchange.com/questions/751922/give-an-equational-proof-vdash-forall-xa-rightarrow-b-equiv-exists) ★

[elementary set theory - Can I deduce one set distributive law from the other? - Mathematics Stack Exchange](https://math.stackexchange.com/questions/4757220/can-i-deduce-one-set-distributive-law-from-the-other) ★

[Robbins algebra - Wikipedia](https://en.wikipedia.org/wiki/Robbins_algebra)

### Formal Verification of Equational Theories

[lo.logic - Formal verification of simple equational proofs (as in Universal Algebra\...)? - MathOverflow](https://mathoverflow.net/questions/71265/formal-verification-of-simple-equational-proofs-as-in-universal-algebra) ★

_(in [Theorem Proving](../Theorem%20Proving/README.md#theorem-proving))_ [Robbins Algebras are Boolean](https://www.cs.unm.edu/~mccune/papers/robbins/) ★ [💭](commentary/Chris%20Pressey.md#robbins-algebras-are-boolean)


### Papers

[Equational Logic and Abstract Algebra](http://sections.maa.org/florida/proceedings/2001/ramsamujh.pdf) ★★★ [💭](commentary/Chris%20Pressey.md#equational-logic-and-abstract-algebra)

[Equational logic, unification and term rewriting](https://www2.math.uu.se/~palmgren/tillog/equlogic07.pdf) ★★

[Field Guide to Equational Logic](https://www.sciencedirect.com/science/article/pii/074771719290013T) ★★ [💭](commentary/Chris%20Pressey.md#field-guide-to-equational-logic)

[Equational Logic (Course Notes, USC, Spring 2017)](https://people.math.sc.edu/mcnulty/alglatvar/equationallogic.pdf) ★★ [💭](commentary/Chris%20Pressey.md#equational-logic-course-notes-usc-spring-2017)

[Euclid's Elements as an Equational Theory](http://boole.stanford.edu/pub/USyd2015.pdf) ★

[Meadows and the Equational Specification of Division](https://arxiv.org/abs/0901.0823v1) ★

[Survey of the Equational Programming Project](https://people.cs.uchicago.edu/~odonnell/OData/Technical_Papers/Survey_ELP/description.html) ★ [💭](commentary/Chris%20Pressey.md#survey-of-the-equational-programming-project)

[Programming with Equations](https://www.cs.purdue.edu/cgvlab/www/publications/hoffmann1982programming/) ★ [💭](commentary/Chris%20Pressey.md#programming-with-equations)

_(in [Type Theory](../Type%20Theory/README.md#type-theory))_ Observational Equality, Now! (online @ [strictlypositive.org](http://strictlypositive.org/obseqnow.pdf)) [💭](commentary/Chris%20Pressey.md#observational-equality-now)


### Books

Equational Logic as a Programming Language (online @ [archive.org](https://archive.org/details/equational-logic-as-a-programming-language)) (borrow @ [archive.org](https://archive.org/details/equationallogica0000odon)) ★ [💭](commentary/Chris%20Pressey.md#equational-logic-as-a-programming-language)

Canonical Equational Proofs (borrow @ [archive.org](https://archive.org/details/canonicalequatio0000bach)) [💭](commentary/Chris%20Pressey.md#canonical-equational-proofs)

_(in [Logic](../Logic/README.md#logic))_ Handbook of logic in artificial intelligence and logic programming, Vol 1 (borrow @ [archive.org](https://archive.org/details/handbookoflogici0001unse)) [💭](commentary/Chris%20Pressey.md#handbook-of-logic-in-artificial-intelligence-and-logic-programming-vol-1)